FDL - Nuprl Lemma : pairwise-map

Nuprl Lemma : pairwise-map

T, T':Type{i}, f:(T

T'), L:(T List), P:(T'

T'

{i'}).
(

x,y

map(f;L). P(x,y))

(

x,y

L. P(f(x),f(y)))

Definitions x:A. B(x), , P Q, (x,yL. P(x;y)), x(s1,s2), P & Q, P Q, P Q, {i..j}, t T, i j < k, A B, A, False, Top, x,y. t(x;y)

Lemmas length-map, length wf1, le wf, int seg wf, pairwise wf, map wf, select-map